Inference at * 2 
Iof proof for Lemma member-zip:



1. A : Type
2. B : Type
3. A List
4. u : A
5. v : A List
6. ys:(B List), x:A, y:B. (<x, y>  zip(v;ys))  {(x  v) & (y  ys)}
  ys:(B List), x:A, y:B. (<x, y>  zip([u / v];ys))  {(x  [u / v]) & (y  ys)} 

latex

 by InductionOnList 

latex

 1: 

 1: 7. B List
 1:   x:A, y:B. (<x, y>  zip([u / v];[]))  {(x  [u / v]) & (y  [])}
 2: 

 2: 7. B List
 2: 8. u1 : B
 2: 9. v1 : B List
 2: 10. x:A, y:B. (<x, y>  zip([u / v];v1))  {(x  [u / v]) & (y  v1)}
 2:   x:A, y:B. (<x, y>  zip([u / v];[u1 / v1]))  {(x  [u / v]) & (y  [u1 / v1])}
 .

Definitions

P  Q, {T}, P & Q, (x  l), x:A  B(x), x:AB(x), x:A. B(x), type List, t  T